/*
 * Copyright 2012 Fabian Wenzelmann
 * 
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 * 
 * Recognition-Procedures-for-Boolean-Functions is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 * 
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 * 
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.  If not, see <http://www.gnu.org/licenses/>.
 */

package de.wenzelmf.booleanFunction.main;

import gnu.getopt.Getopt;
import gnu.getopt.LongOpt;

import java.io.BufferedReader;
import java.io.File;
import java.io.FileNotFoundException;
import java.io.FileReader;
import java.io.IOException;
import java.io.StringReader;

import de.wenzelmf.booleanFunction.dnf.DNF;
import de.wenzelmf.booleanFunction.lpb.combinatorial.solver.ClassicalTreeSolver;
import de.wenzelmf.booleanFunction.lpb.combinatorial.solver.DoubleSolverInformation;
import de.wenzelmf.booleanFunction.lpb.combinatorial.solver.MinimumChooser;
import de.wenzelmf.booleanFunction.lpb.combinatorial.solver.TreeSolver;
import de.wenzelmf.booleanFunction.lpb.util.ConversionException;
import de.wenzelmf.booleanFunction.lpb.util.LPB;
import de.wenzelmf.booleanFunction.lpb.util.LPBCombinatorialConstants;
import de.wenzelmf.booleanFunction.parser.BFParser;
import de.wenzelmf.booleanFunction.parser.DIMACSParser;
import de.wenzelmf.booleanFunction.parser.DNFFileReader;
import de.wenzelmf.booleanFunction.parser.ParseException;



public class Main
{
	/**
	 * The main method.
	 * 
	 * @param args Command line arguments. 
	 */
	public static void main(String[] args)
	{
		String progName = "recognition procedures for Boolean functions";
		String version = "0.9.1";
		String url = "http://code.google.com/p/recognition-procedures-for-boolean-functions/";
		boolean lpbConvertMode = false;
		File file = null;
		File dimacsFile = null;
		LongOpt helpOpt = new LongOpt("help", LongOpt.NO_ARGUMENT, null, 'h');
		LongOpt versionOpt = new LongOpt("version", LongOpt.NO_ARGUMENT, null, 'v');
		LongOpt convertOpt = new LongOpt("convertlpb", LongOpt.OPTIONAL_ARGUMENT,
				null, 'c');
		LongOpt fileOpt = new LongOpt("file", LongOpt.REQUIRED_ARGUMENT, null, 'f');
		LongOpt dimacsOpt = new LongOpt("dimacs", LongOpt.REQUIRED_ARGUMENT, null, 'd');
		
		
		LongOpt[] longOpts = {helpOpt, versionOpt, convertOpt, fileOpt, dimacsOpt};
		Getopt g = new Getopt(progName, args, "hvc::f:d:", longOpts);
		
		int c;
		String arg;
		while((c = g.getopt()) != -1)
		{
			switch(c)
			{
			case 0:
			case 1:
			case 2:
				// should not happen
		        break;
			case 'h':
				System.out.println("Convert DNFs to LPBs by");
				System.out.println("\t-convertlpb LPBS");
				System.out.println("This will convert all LPBs following the convertlpb option.");
				
				System.out.println("You can also specify a file that contains in each line a DNF by");
				System.out.println("\t-convertlpb --file FILENAME");
				System.out.println();
				System.out.print("You can also use shortcuts like -c (for \"convertlpb\") and ");
				System.out.println("-f for file.");
				return;
			case 'v':
				System.out.println(progName + " (version " + version + ")");
				System.out.print("See " + url);
				System.out.println(" for more information.");
				System.out.println();
				System.out.println("Copyright (C) 2011, 2012 Fabian Wenzelmann");
				System.out.println("Published under GPL version 3, see file COPYING.");
				return;
			case 'c':
				arg = g.getOptarg();
				lpbConvertMode = true;
				// if we add different convert modes add this behavior
				// atm we ignore the argument
				break;
			case 'f':
				file = new File(g.getOptarg());
				break;
			case 'd':
				dimacsFile = new File(g.getOptarg());
				break;
			case '?':
				return;
			}
		}
		if(!lpbConvertMode)
		{
			System.out.println("Nothing to do.");
			return;
		}
		if(file != null)
		{
			// parse file and convert all DNFs in it
			DNFFileReader reader = null;
			try
			{
				reader = new DNFFileReader(file);
			} catch (IOException e)
			{
				System.err.println("Unable to open file \"" + file + "\". Error message:");
				e.printStackTrace();
				return;
			}
			DNF dnf = null;
			try
			{
				dnf = reader.next();
			}
			catch(IOException e)
			{
				System.err.println("Unable to read next DNF from file \"" + file + "\". Error message:");
				e.printStackTrace();
			}
			while(dnf != null)
			{
				// try to convert the DNF
				TreeSolver solver = new TreeSolver(false, new ClassicalTreeSolver(new MinimumChooser(), new DoubleSolverInformation()));
				convertLPB(dnf, solver);
				try
				{
					dnf = reader.next();
				}
				catch(IOException e)
				{
					System.err.println("Unable to read next DNF from file \"" + file + "\". Error message:");
					e.printStackTrace();
					dnf = null;
				}
			}
		}
		
		if(dimacsFile != null)
		{
			BufferedReader reader = null;
			try
			{
				reader = new BufferedReader(new FileReader(dimacsFile));
			}
			catch (FileNotFoundException e)
			{
				System.err.println("Unable to read file \"" + dimacsFile + "\". Error message:");
				e.printStackTrace();
			}
			DIMACSParser parser = new DIMACSParser(reader, LPBCombinatorialConstants.defaultClauseFactory,
					LPBCombinatorialConstants.defaultDNFFactory);
			DNF dnf = null;
			try
			{
				dnf = parser.DIMACSDNF();
			}
			catch (ParseException e)
			{
				System.err.println("Unable to read file \"" + dimacsFile + "\" as DIMACS DNF. Error message:");
				e.printStackTrace();
				return;
			}
			TreeSolver solver = new TreeSolver(false, new ClassicalTreeSolver(new MinimumChooser(), new DoubleSolverInformation()));
			convertLPB(dnf, solver);
		}
		
		// parse all following arguments as DNFs
		BFParser parser = new BFParser(new StringReader(""));
		parser.setClauseFactory(LPBCombinatorialConstants.defaultClauseFactory);
		parser.setDNFFactory(LPBCombinatorialConstants.defaultDNFFactory);
		for (int i = g.getOptind(); i < args.length ; i++)
		{
			parser.ReInit(new StringReader(args[i]));
			DNF dnf = null;
			try
			{
				dnf = parser.DNF();
			}
			catch (ParseException e)
			{
				System.err.println("Unable to parse \"" + args[i] + "\" as DNF. Error message:");
				e.printStackTrace();
			}
			TreeSolver solver = new TreeSolver(false, new ClassicalTreeSolver(new MinimumChooser(), new DoubleSolverInformation()));
			convertLPB(dnf, solver);
		}
	}
	
	/**
	 * Try to convert the DNF with the solver.
	 * 
	 * Prints the result if conversion was successful and prints an error message otherwise.
	 */
	private static void convertLPB(DNF dnf, TreeSolver solver)
	{
		try
		{
			LPB lpb = solver.convert(dnf);
			System.out.println(lpb);
		}
		catch(ConversionException e)
		{
			System.err.println("Unable to convert the DNF \"" + dnf.toSetString() + "\". Error message:");
			e.printStackTrace();
		}
	}
	
}
